Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

arch-split: Requalify enhancements #788

Merged
merged 4 commits into from
Jul 23, 2024
Merged

Conversation

Xaphiosis
Copy link
Member

Reviewers:🦆🦆🦆

Probably best to review this commit-by-commit (they don't overlap). The "asms -> assms" commit generates a bit of diff noise.

Otherwise, besides a sanity check of ML code, documentation and style, what I would like help with:

  • I added a bunch of documentation/examples to Requalify.thy
    • not overly happy with exporting all those symbols to anyone who imports Requalify
    • the arch section of the examples won't work unless L4V_ARCH is set
    • should we move all this out to an example file?
    • what do I do with the old examples? They are somewhat opaque for anyone trying to understand what's going on, but my examples don't thoroughly test an arch-split-like situation to ensure that the right constants/types/thms end up under the right names and proofs succeed
  • I have zero idea how I could detect a name collision when exporting into a locale, thoughts?
  • I'm not a fan of that collision resolution global. naming workaround, but I documented it anyway. I guess we'll always have situations where we do an interpretation of Arch inside a context and so name order matters?

The docs/arch-split needs an update for better practices, but I want to leave that for after I deploy some of this tech and see what the best practices actually are.

@Xaphiosis
Copy link
Member Author

This addresses #777

@lsf37
Copy link
Member

lsf37 commented Jul 11, 2024

  • I added a bunch of documentation/examples to Requalify.thy

    • not overly happy with exporting all those symbols to anyone who imports Requalify

The examples are good, but it'd be nice to avoid the name space pollution, yes. Does experiment begin .. end help anything? If not, moving the examples to a separate test file is probably what we should do.

  • the arch section of the examples won't work unless L4V_ARCH is set

That's fine from my side. I think we can assume that L4V_ARCH is always set when we run these theories.

  • should we move all this out to an example file?

If experiment doesn't work here, then I would say yes.

  • what do I do with the old examples? They are somewhat opaque for anyone trying to understand what's going on, but my examples don't thoroughly test an arch-split-like situation to ensure that the right constants/types/thms end up under the right names and proofs succeed

Happy to leave them in for now. We can improve them some other time if we feel like it.

  • I have zero idea how I could detect a name collision when exporting into a locale, thoughts?

None currently. Can you elaborate on which technical bits we are missing?

  • I'm not a fan of that collision resolution global. naming workaround, but I documented it anyway. I guess we'll always have situations where we do an interpretation of Arch inside a context and so name order matters?

We do have some few of these global. constants, but not a lot. For the few times we're using it, I think the mechanism is fine, and it's good that it is now properly documented, because I had not actually understood how we achieve that.

The docs/arch-split needs an update for better practices, but I want to leave that for after I deploy some of this tech and see what the best practices actually are.

👍

@Xaphiosis
Copy link
Member Author

  • should we move all this out to an example file?

If experiment doesn't work here, then I would say yes.

locale and context can't be used inside experiment, so I guess I'll move it.

  • I have zero idea how I could detect a name collision when exporting into a locale, thoughts?

None currently. Can you elaborate on which technical bits we are missing?

You'd have to take a look at the ML code for more context, and the bit in the examples where it says there is currently no warning on name collisions into locales.

First, the results of Parse.opt_target is something we hand to Toplevel.local_theory. If it's NONE, great, we can check the base name against a lookup in the global theory. If it isn't NONE though, we get an xstring * Position.T, i.e. the locale's parsed name (e.g. Requalify_Example2). I don't know how to go from a locale name in a string to somehing I can search in.

Second, there is a worse issue. Say you have this:

locale Arch

context Arch begin
  lemma aaa: "2 = (2 :: nat)" by simp
end

context Arch begin global_naming AARCH64
  lemma aaa: "1 = (1 :: nat)" by simp
end

thm Arch.aaa (* 2 = 2 *)
thm AARCH64.aaa (* 1 = 1 *)

locale Moo
requalify_facts (in Moo) AARCH64.aaa (* this is fine *)
thm Moo.aaa (* 1 = 1 *)
requalify_facts (in Moo) Arch.aaa (* this is not fine, we'd like a warning, Moo already has aaa *)
thm Moo.aaa (* 2 = 2 *)

and then the total disaster area, which is where I don't even know what to do, and sadly this might come up in arch-split:

(* dump AARCH64.aaa into Arch locale now, note how we don't have to specify AARCH64 *)
requalify_facts (in Arch) aaa (* no warning, no qualification needed either! *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) Arch.aaa (* still no warning, but I guess we'd want one *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) aaa (* still no warning, but we definitely want one *)
thm Arch.aaa (* 1 = 1 *)

Do you see the problem? In the Moo case you can check if it's already there, but in the Arch case it is already there, as witnessed by being able to pull AARCH64.aaa without the qualification. The above example has another Arch.aaa that is additionally there, confusing things further.

@Xaphiosis
Copy link
Member Author

Xaphiosis commented Jul 11, 2024

Moved Requalify tests into lib/test/Requalify_Test.thy and rebased

@lsf37
Copy link
Member

lsf37 commented Jul 16, 2024

First, the results of Parse.opt_target is something we hand to Toplevel.local_theory. If it's NONE, great, we can check the base name against a lookup in the global theory. If it isn't NONE though, we get an xstring * Position.T, i.e. the locale's parsed name (e.g. Requalify_Example2). I don't know how to go from a locale name in a string to somehing I can search in.

It's been a very long time since I did anything with this (usually you get the local_theory from the top-level command), but if b is your xstring * Position.T, then Target_Context.context_begin_named_cmd [] b : theory -> local_theory looks like it might fit the bill. At least it is also used by context b begin .. end.

Second, there is a worse issue. Say you have this:

locale Arch

context Arch begin
  lemma aaa: "2 = (2 :: nat)" by simp
end

context Arch begin global_naming AARCH64
  lemma aaa: "1 = (1 :: nat)" by simp
end

thm Arch.aaa (* 2 = 2 *)
thm AARCH64.aaa (* 1 = 1 *)

locale Moo
requalify_facts (in Moo) AARCH64.aaa (* this is fine *)
thm Moo.aaa (* 1 = 1 *)
requalify_facts (in Moo) Arch.aaa (* this is not fine, we'd like a warning, Moo already has aaa *)
thm Moo.aaa (* 2 = 2 *)

and then the total disaster area, which is where I don't even know what to do, and sadly this might come up in arch-split:

(* dump AARCH64.aaa into Arch locale now, note how we don't have to specify AARCH64 *)
requalify_facts (in Arch) aaa (* no warning, no qualification needed either! *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) Arch.aaa (* still no warning, but I guess we'd want one *)
thm Arch.aaa (* 1 = 1 *)
requalify_facts (in Arch) aaa (* still no warning, but we definitely want one *)
thm Arch.aaa (* 1 = 1 *)

Do you see the problem? In the Moo case you can check if it's already there, but in the Arch case it is already there, as witnessed by being able to pull AARCH64.aaa without the qualification. The above example has another Arch.aaa that is additionally there, confusing things further.

I don't have any immediate solutions for these, but given that we had no warnings at all before, it's not catastrophic if we start small and improve these over time.

Copy link
Member

@corlewis corlewis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very nice, especially with how generic you have managed to make it with so much code reuse. Thank you for the comments and examples, they are very helpful.

I haven't thought of anything so far that could help with the naming collisions in locales, but I agree with @lsf37 that this is already such a big improvement that it can be left for later.

Comment on lines 48 to 61
(* Locate global fact matching supplied name.
When we specify a fact name that resolves to a global name, return the normal fact lookup result.
Note: Locale_Name.fact_name outside the locale resolves to a global name.

When we are inside a locale, the lookup is more interesting. Supplying "short_name" will result
in "local.short_name", which we then need to match to some name in the global context. We do
this by going through *all* the fact names in the current context, searching for matches
of the form "X.Y.short_name", where we hope X is some theory, and Y is some locale.

Since "X.Y.short_name" is not sufficiently unique, we must also check that the theorems under
the discovered name match the ones under "local.short_name". *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for this very helpful comment (and for all the other comments you've added).

>> (fn (target,bs) =>
Toplevel.local_theory NONE target (fn lthy =>
let
(* ([aliasing][,] [A|H]) in that order *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Out of curiosity, why do you want to fix that order? I think it would be slightly easier to implement and probably not need the split between generic_options and arch_options if you didn't.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is because of n+1-flavour soup. If I allow both, we will see someone in the future discovering that they can write (H, aliasing) while everyone else writes it the other way around. I'm fine to change that order, but for some reason I got it stuck into my head that I only want one. What do you think?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm easy. Fixing it to one order does reduce the number of styles, but it also can be frustrating to use if you don't remember what order it should be and are only getting the typical Isabelle "bad syntax" error message.

Would it make sense to try to give an informative error message when the order is wrong?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll be honest, I do not know how one does that.

Copy link
Member

@lsf37 lsf37 Jul 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have never tried this in Isabelle, but usually you'd explicitly parse the wrong order and then produce an error message (I guess throw an exception with a useful message?)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can give this a go later I guess.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The "list of options" thing is also weird to me. I mean, someone could do (A, aliasing, H) if it's a list, so the error checking becomes more complex.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or even worse: (A, H, aliasing, A, A, H, A) ...

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we don't care about order, then it's a case of sort|uniq and then error if it's both A and H, but if we care about order I'd need to check for duplicates... I am not getting a clear image of good interface here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we'll leave this for another time. Have to redirect resources to arch-splitting.

lib/Requalify.thy Outdated Show resolved Hide resolved
lib/Requalify.thy Outdated Show resolved Hide resolved
i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms
("asms" is rarely expected outside of ML code)

Signed-off-by: Rafal Kolanski <[email protected]>
* add warnings when exporting a name that already exists in theory
  context, suppressable by `(aliasing)` option
* add `arch` variants of requalify commands that implicitly add the
  value of L4V_ARCH before whatever you give them, with optional
  suffixes for abstract (A) and Haskell (H) spec global naming.
* write hopefully-understandable documentation with commented examples

Signed-off-by: Rafal Kolanski <[email protected]>
Also document that requalify commands will issue warnings.

Signed-off-by: Rafal Kolanski <[email protected]>
Stops namespace pollution, allows us to use Arch locale as example.

Signed-off-by: Rafal Kolanski <[email protected]>
@Xaphiosis Xaphiosis merged commit bc948e3 into seL4:master Jul 23, 2024
12 of 14 checks passed
@Xaphiosis Xaphiosis deleted the arch_split branch July 23, 2024 06:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement proof engineering nicer, shorter, more maintainable etc proofs
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants